import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.FileWriter;
import java.io.FilenameFilter;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.Scanner;

/**
 * <h1>Classe : GrapheOriente</h1>
 * 
 * Classe permettant de manipuler des graphes orientés.
 * On peut :
 * <ul>
 * <li>Créer un graphe orienté à partir d'un fichier texte au format 'graphiz'.</li>
 * <li>Vérifier si un graphe a un cycle hamiltonien en O (n.k) (n sommets, k arètes) à partir d'un certificat.</li>
 * <li>Rechercher un cycle hamiltonien dans un graphe orienté avec un algorithme 'back track'.</li>
 * <li>Réduire une expression booléenne de forme 3-SAT en un cycle hamiltonien</li>
 * </ul>
 */
public class GrapheOriente {
	private ArrayList<Sommet> sommets;
	private ArrayList<Sommet> certificat;
	private int nbVariables=0;
	private int nbClauses=0;
	private int nbSommetsParLigne=0;
	public ArrayList<Sommet> cycle;
	
	/**
	 * <h1>Constructeur : GrapheOriente</h1>
	 * 
	 * Créer un graphe vide.
	 */
	private GrapheOriente(){
		this.sommets = new ArrayList<>();
		this.cycle = new ArrayList<>();
	}
	
	/**
	 * <h1>Constructeur : GrapheOriente</h1>
	 * Créer un graphe orienté à partir d'un fichier type 'graphiz'
	 * 
	 * @param fichier Le fichier où est contenu le graphe orienté.
	 */
	public GrapheOriente(String fichier){
		this();
		this.importeFichierGraphe(fichier);
	}
	
	/**
	 * <h1>Méthode : verificateur</h1>
	 * 
	 * Vérifie si le certificat fourni forme un cycle hamiltonien dans le graphe.
	 * Le paramètre doit être une ArrayList des sommets par lesquels passe le cycle dans l'ordre de la liste
	 * 
	 * @param certificat Le certificat à tester (liste de sommet)
	 * @return <ul><li>Vrai Si le certificat correspond à un cycle hamiltonien</li><li>Faux Si le certificat n'est pas un cycle hamiltonien</li></ul>
	 */
	public boolean verificateur(ArrayList<Sommet> certificat){
		this.certificat=certificat;
		return this.verificateur();
	}
	
	/**
	 * <h1>Méthode : verificateur</h1>
	 * 
	 * Vérifie si le certificat fourni est un cycle hamiltonien du graphe.
	 * Le paramètre doit être une string contenant les sommets par lesquels passe le cycle dans l'ordre et séparé par des espaces
	 * 
	 * @param certificat Le certificat à tester (liste de points d'une string)
	 * @return <ul><li>Vrai Si le certificat correspond à un cycle hamiltonien</li><li>Faux Si le certificat n'est pas un cycle hamiltonien</li></ul>
	 */
	public boolean verificateur(String certif){
		this.importeCertificat(certif);
		return this.verificateur();
	}
	
	/**
	 * <h1>Méthode : importeCertificatFichier</h1>
	 * 
	 * Importe un certificat contenu dans le fichier donné en paramètre
	 * Ce fichier doit se composer de liste de sommet écrit sur une ligne et séparé par des espaces.
	 * 
	 * @param nomFichier Le lien vers le fichier qui contient le certificat.
	 */
	public void importeCertificatFichier(String nomFichier){
		try {
			BufferedReader br = new BufferedReader(new InputStreamReader(new FileInputStream(nomFichier)));
			this.importeCertificat(br.readLine());
			br.close();
		} catch (IOException e) {
			e.printStackTrace();
		}
	}
	
	/**
	 * <h1>Méthode importeCertificat</h1>
	 * 
	 * Créer un certificat avec la liste de sommet donné dans la chaine de caractères en paramètre
	 * 
	 * @param certif Une string de forme "[sommet1] [sommet2] [sommet3]"
	 */
	public void importeCertificat(String certif){
		boolean sommetExist;
		this.certificat = new ArrayList<>();
		for(String s :certif.split(" ")){
			sommetExist = false;
			for(Sommet som : this.sommets){
				if(som.toString().equals(s)){
					sommetExist = true;
					this.certificat.add(som);
					continue;
				}
			}
			if(!sommetExist){
				this.certificat.add(new Sommet(s));
			}
		}
	}
	
	/**
	 * <h1>Méthode verificateur</h1>
	 * 
	 * Vérifie si le certificat importé est un cycle hamiltonien du graphe
	 * 
	 * @return <ul><li>Vrai Si le certificat correspond à un cycle hamiltonien</li><li>Faux Si le certificat n'est pas un cycle hamiltonien</li></ul>
	 */
	public boolean verificateur(){
		int compteurSommet = 1;
		int[] sommetCompteur = new int [this.sommets.size()];
		
		if(this.certificat==null){
			return false;
		}
		
		if(this.certificat.size()!=this.sommets.size()+1){
			return false;
		}
		
		if(!this.certificat.get(0).equals(this.certificat.get(this.certificat.size()-1))){
			return false;
		}
		
		for(int i = 0; i<this.sommets.size(); ++i){
			sommetCompteur[i] = 0;
		}
		
		for(int i = 0; i<this.sommets.size(); ++i){
			if(sommetCompteur[Integer.parseInt(this.certificat.get(i).toString())-1] >= 1){
				return false;
			}
			sommetCompteur[Integer.parseInt(this.certificat.get(i).toString())-1] ++;
		}
		
		/*
		 * Parcours le graphe en suivant le certificat
		 */
		
		for(int i = 1; i< this.certificat.size(); ++i){
			Sommet depart = this.certificat.get(i-1);
			Sommet arrive = this.certificat.get(i);
			
			for(Arete a : depart.getAretes()){
				if(a.arrive.equals(arrive)){
					++compteurSommet;
					continue;	
				}
			}
		}
		
		
		/*
		 * Si le nombre de sommets parcouru correspond à la taille du certificat, celui ci est valide
		 */
		
		if(compteurSommet == this.certificat.size())
			return true;
		return false;
	}
	
	
	
	
	/**
	 * <h1>Méthode : solver</h1>
	 * 
	 * Permet de savoir si un graphe possède un cycle hamiltonien ou non.
	 * 
	 * @return Vrai Si un cycle hamiltonien a été trouvé.
	 * @return Faux Si le garphe ne contient pas de cycle hamiltonien.
	 */
	public boolean solver(){
		ArrayList<Sommet>mesSommets = new ArrayList<>();
		
		for(Sommet s  : this.sommets){
			mesSommets.add(s);
		}
		
		/*
		 * (this.sommets.size()-this.nbClause-2) correspond au sommet 'début'
		 */
		
		return this.solver(this.sommets.get(this.sommets.size()-this.nbClauses-2), mesSommets);
	}
	
	/**
	 * <h1>Méthode : solver</h1>
	 * 
	 * Algorithme récursif avec 'back track', permettant de savoir si un cycle hamiltonien ou pas existe dans le graphe.
	 * 
	 * @param depart Le sommet sur lequel s'applique la recherche
	 * @param sommetsRestants La liste des sommets sur lesquels la recherche ne s'est pas encore appliquée
	 * @return Vrai Si un cycle hamiltonien a été trouvé.
	 * @return Faux Si le garphe ou le sous graphe concerné ne contient pas de cycle hamiltonien.
	 */
	private boolean solver(Sommet depart, ArrayList<Sommet> sommetsRestants){
		sommetsRestants.remove(depart);
		this.cycle.add(depart);
		
		/*
		 * Condition de sortie de l'algo recursif : on est passé par tous les sommets
		 */
		
		if(sommetsRestants.size()==0){
			
			/*
			 * On regarde si le dernier sommet restant est connecté au premier
			 */
			
			for(Arete a : depart.getAretes()){
				if(a.arrive.equals(this.sommets.get(this.sommets.size()-this.nbClauses-2))){
					this.cycle.add(this.sommets.get(this.sommets.size()-this.nbClauses-2));
					return true;
				}
			}
			this.cycle.remove(depart);
			sommetsRestants.add(depart);
			return false;
		}
		
		/*
		 * Test le parcours par toutes les arètes du sommet encore disponible
		 * Rappel de l'algorithme sur elles
		 */
		Object[] soms = sommetsRestants.toArray();
		for(Arete a : depart.getAretes()){
			
			/*
			 * On utilise une copie de la liste pour éviter une utilisation concourante
			 */
			
			for(Object o : soms){
				Sommet s = (Sommet)o;
				if(s.equals(a.arrive)){
					if(this.solver(s, sommetsRestants)){
						return true;
					}
				}
			}
		}
		
		sommetsRestants.add(depart);
		this.cycle.remove(depart);
		return false;
	}
	
	/**
	 * <h1>Méthode : importeFichierGraphe</h1>
	 * 
	 * Importe le graphe contenu dans un fichier texte.
	 * L'encodage d'un graphe doit être comme indiquer ci-dessous :
	 * 
	 * <b>digraph{<b>
	 * sommet1 sommet2 sommet3
	 * sommet1->sommet2
	 * sommet2->sommet3
	 * <b>}<b>
	 * 
	 * Le nombre d'arète n'est pas limité.
	 * 
	 * @param filename Le cheminb vers le fichier àimporter.
	 */
	public void importeFichierGraphe(String filename){
		
		String ligne = "";
		BufferedReader br;
		
		try {
			br = new BufferedReader(new InputStreamReader(new FileInputStream(filename)));
			ligne = br.readLine();
			ligne = br.readLine();
			/*
			 * Créer tous les sommets.
			 */
			
			for(String s :ligne.split(" ")){
				this.sommets.add(new Sommet(s));
			}
			
			ligne = br.readLine();
			
			/*
			 * Ajoute les arètes.
			 */
			
			while(!ligne.equals("}")){
				for(Sommet sDepart : this.sommets){
					if(sDepart.equals(new Sommet(ligne.split("->")[0]))){
						for(Sommet sArrive : this.sommets){
							if(sArrive.equals(new Sommet(ligne.split("->")[1]))){
								sDepart.ajouteArete(sArrive);
								break;
							}
						}
					}
				}
				
				ligne = br.readLine();
				//System.out.println(ligne);
			}
			br.close();
			
		} catch (FileNotFoundException e) {
			System.err.println("Fichier non trouv� !");;
		}
		catch (IOException e) {
			e.printStackTrace();
		}
	}
	
	/**
	 * <h1>Méthode toString</h1>
	 * 
	 * Retourne une représentation du graphe sous forme de string.
	 * @return graphe La représentation du graphe en chaine de caractère.
	 */
	public String toString(){
		String retour = "";
		for(Sommet s : this.sommets)
			retour += s+" ";
		for(Sommet s : this.sommets){
			for(Arete a : s.getAretes()){
				retour+="\n"+a;
			}
		}
		return retour;
	}
	
	/**
	 * <h1>Méthode : reducteur</h1>
	 * 
	 * Créer un graphe orienté àpartir de l'expression booléenne de forme 3-SAT présente dans le fichier en paramètre
	 * 
	 * @param cheminFichier
	 */
	private void reducteur(String cheminFichier){		
		
		File fichier = new File(cheminFichier);
		try {
			BufferedReader br = new BufferedReader(new InputStreamReader(new FileInputStream(fichier)));

			br.readLine();
			String ligne = br.readLine();
			
			this.nbClauses = Integer.parseInt(ligne.split(" ")[1]);
			this.nbVariables = Integer.parseInt(ligne.split(" ")[0]);
			this.nbSommetsParLigne = 4*nbClauses;
			int numeroSommet = 0;
			
			for(int i=0 ; i< nbVariables; ++i){
				
				for(int j = 0; j< nbSommetsParLigne; ++j){
					
					this.sommets.add(new Sommet(++numeroSommet+""));
					
				}
			}
			
			numeroSommet = 0;
			
			/*
			 * Créer toutes les lignes des variables de l'expression.
			 * Fait un double lien pour tous les sommets de chaque ligne.
			 * Lie les extrémités des lignes à celles de la suivante.
			 */
			
			for(int j = 1; j <= nbVariables; ++j){
				
				for(int i = 1; i <= nbSommetsParLigne; ++i){				
					
					if(numeroSommet<this.sommets.size()-1){
						this.sommets.get(numeroSommet).ajouteArete(this.sommets.get(numeroSommet+1));
						if(numeroSommet%nbSommetsParLigne!=0){
							this.sommets.get(numeroSommet).ajouteArete(this.sommets.get(numeroSommet-1));
						}else if(numeroSommet+nbSommetsParLigne<this.sommets.size()-1){
								this.sommets.get(numeroSommet).ajouteArete(this.sommets.get(numeroSommet+nbSommetsParLigne));
								this.sommets.get(numeroSommet).ajouteArete(this.sommets.get(numeroSommet+(nbSommetsParLigne*2)-1));
						}
						else if ((numeroSommet)%nbSommetsParLigne == 0){
							if(numeroSommet+nbSommetsParLigne<this.sommets.size()){
								this.sommets.get(numeroSommet).ajouteArete(this.sommets.get(numeroSommet+nbSommetsParLigne));
							}
						}
						if((numeroSommet+1)%nbSommetsParLigne==0){
							this.sommets.get(numeroSommet).ajouteArete(this.sommets.get(numeroSommet+nbSommetsParLigne));
						}
					}
					++numeroSommet;
				}
			}
			
			/*
			 * Créer et lie le sommet du début et de la fin avec les 'quatre extrémités' du graphe des variables
			 */
			
			Sommet debut = new Sommet("Debut");
			Sommet fin = new Sommet("Fin");
			
			fin.ajouteArete(debut);
			
			debut.ajouteArete(this.sommets.get(nbSommetsParLigne-1));
			debut.ajouteArete(this.sommets.get(0));
			
			this.sommets.get(this.sommets.size()-1).ajouteArete(fin);
			this.sommets.get(this.sommets.size()-nbSommetsParLigne).ajouteArete(fin);
			
			this.sommets.add(debut);
			this.sommets.add(fin);
			
			/*
			 * Ajout des clauses et de leurs liens.
			 */
			for(int i = 0; i<= nbClauses; ++i){				
				
				Sommet s = new Sommet("C"+(i+1));
				
				String[] clause = br.readLine().split(" ");
				
				if(clause[0].equals("}")){
					break;
				}
				
				boolean sensInverse = false;
				
				for(String variable : clause){
					if(variable.startsWith("-")){
						sensInverse = true;
						variable = variable.substring(1);
					}
					
					Sommet departClause = this.sommets.get(i*2+(Integer.parseInt(variable)-1)*nbSommetsParLigne+2);
					Sommet arriveClause = this.sommets.get(((i*2+(Integer.parseInt(variable)-1)*nbSommetsParLigne))+3);
					
					if(sensInverse){
						arriveClause.ajouteArete(s);
						s.ajouteArete(departClause);
						sensInverse = false;
					}else{
						departClause.ajouteArete(s);
						s.ajouteArete(arriveClause);
					}
				}
				this.sommets.add(s);
			}
			
			br.close();
		} catch (IOException e) {
			e.printStackTrace();
		}
	}
	
	/**
	 * <h1>fonction : expressionTroisSATToGraphe</h1>
	 * 
	 * Fonction 'factory' permettant de créer un graphe à partir d'une expression 3-SAT contenue dans un fichier texte.
	 * 
	 * @param fichier Chemin du fichier contenant l'expression 3-SAT
	 * @return Le graphe correspondant � l'expression 3-SAT
	 */
	public static GrapheOriente expressionTroisSATToGraphe(String fichier){
		GrapheOriente go = new GrapheOriente();
		go.reducteur(fichier);
		return go;
	}
	
	/**
	 * <h1>Méthode : exportGraphviz</h1>
	 * 
	 * Exporte le graphe courant dans un fichier lisible dans la syntaxe graphviz
	 */
	public void exportGraphviz(){
		FileWriter fichier;
		try {
			fichier = new FileWriter("sat");
			BufferedWriter bw = new BufferedWriter(fichier);
			
			/*
			 * Mise en page pour alligner les variables ect
			 */
			
			bw.write("digraph{");
			bw.newLine();
			
			int j=0,i=0,m=0;
			for(j = 0 ; j<this.nbVariables; ++j){
				bw.write("{rank=same; ");
				for(i = 0 ; i<this.nbSommetsParLigne; ++i){
					bw.write(this.sommets.get(m).toString()+" ");
					bw.flush();
					++m;
				}
				bw.newLine();
				bw.write("rankdir=LR\n}");
			}
			
			bw.write("{rank=min; ");
			bw.write(this.sommets.get(m).toString()+" ");
			bw.flush();
			bw.write("}");
			bw.newLine();
			
			++m;
			
			bw.write("{rank=max; ");
			bw.write(this.sommets.get(m).toString()+" ");
			bw.flush();
			bw.write("}");
			
			++m;
			
			bw.write("{rank=same; ");
			for(;m < this.sommets.size(); ++m){
				bw.write(this.sommets.get(m).toString()+" ");
				bw.flush();
			}
			bw.write("}");
			
			
			for(Sommet s : this.sommets){
				for(Arete a : s.getAretes()){
					bw.newLine();
					bw.write(a.toString());
					
					/*
					 * Colorie le cycle en rouge dans le graphe de sortie
					 */
					
					for(int k = 0; k<this.cycle.size()-1; ++k){
						if(this.cycle.get(k).equals(a.depart)){
							if(this.cycle.get(k+1).equals(a.arrive)){
								bw.write(" [color = red]");
							}
						}
					}
				}
			}
			
			bw.newLine();
			bw.write("}");
			
			bw.close();
			
		} catch (IOException e) {
			e.printStackTrace();
		}
	}
	
	/**
	 * Main pour tester les méthodes.
	 */
	public static void main(String[] args){
		/*
		GrapheOriente go2 = GrapheOriente.expressionTroisSATToGraphe("troissat");
		System.out.println("L'expression bool�enne de forme 3-SAT pr�sente un cycle Hamiltonien : "+go2.solver());
		go2.exportGraphviz();
		System.out.println(go2.cycle);
		//System.out.println(go2.cycle);
		 */
		/*
		GrapheOriente go = new GrapheOriente("graphes");
		System.out.println(go.toString());
		//go.importeCertificat("4 1 5 2 3 4");
		go.importeCertificat("2 3 4 1 3");
		System.out.println(go.certificat);
        System.out.println(go.verificateur());
		*/
		Scanner stdin = new Scanner(System.in);
		
		String os = System.getProperty("os.name");
		
		GrapheOriente monGraphe = null;
		
		File file;
		
		if(os.startsWith("Linux")){
			file = new File("./Instances");
		}else if(os.startsWith("Windows")){
			file = new File("../Instances");
		}else{
			System.out.println("Système non detecte, cela peut mener à une erreur d'emplacement du fichier");
			file = new File("./Instances");
		}

		System.out.println("Que voulez vous faire ?"
				+ "\ni    - Importer un graphe depuis un fichier (type graphviz)"
				+ "\nr    - Réduire une expression booleene contenue dans un fichier"
				+ "\nexit - quitter");
		
		String commande  = stdin.nextLine();
		
		while(!commande.startsWith("exit")){
			
			
			if(commande.startsWith("i")){
				
				System.out.println("Importer graphe : ");
				
				String[] mesFichiers = file.list(new FilenameFilter() {
					
					@Override
					public boolean accept(File dir, String name) {
						return name.startsWith("instance-HamiltonienOriente");
					}
				});
				
				for(int i = 0; i<mesFichiers.length ; ++i){
					System.out.println(i+" - "+mesFichiers[i]);
				}
				
				commande = stdin.nextLine();
				
				monGraphe = new GrapheOriente(file.getAbsolutePath()+File.separator+mesFichiers[Integer.parseInt(commande)]);
				
				System.out.println(""
						+ "\nch   - Chercher un cycle hamiltonien"
						+ "\nac   - Affiche le cycle en console"
						+ "\ne    - Exporter le graphe dans un fichier type graphviz"
						+ "\nic   - Importer un certificat pour ce graphe"
						+ "\nv    - Lancer le vérificateur de ce certificat"
						+ "\ntc   - Taper un certificat au clavier"
						+ "\nexit - quitter");
				
				commande = stdin.nextLine();
				
				while(!commande.startsWith("exit")){
					
					if(commande.startsWith("ch")){
						System.out.println("Le graphe possède un cycle hamiltonien : "+monGraphe.solver());
					}
					
					if(commande.startsWith("ac")){
						if(monGraphe.cycle.size()==0){
							monGraphe.solver();
						}
						System.out.println("Cycle : "+monGraphe.cycle);
					}
					
					if(commande.startsWith("e")){
						monGraphe.exportGraphviz();
					}
					
					if(commande.startsWith("v")){
						System.out.println("Le certificat est "+monGraphe.verificateur()+" pour le graphe");
					}
					
					if(commande.startsWith("ic")){
						
						System.out.println("Importer certificat : ");
						
						mesFichiers = file.list(new FilenameFilter() {
							
							@Override
							public boolean accept(File dir, String name) {
								return name.startsWith("certificat-");
							}
						});
						for(int i = 0; i<mesFichiers.length ; ++i){
							System.out.println(i+" - "+mesFichiers[i]);
						}
						
						commande = stdin.nextLine();
						
						System.out.println(file.getAbsolutePath()+File.separator+mesFichiers[Integer.parseInt(commande)]);
						
						File f = new File(file.getAbsolutePath()+File.separator+mesFichiers[Integer.parseInt(commande)]);
						System.out.println(f.exists());						
						monGraphe.importeCertificatFichier(file.getAbsolutePath()+File.separator+mesFichiers[Integer.parseInt(commande)]);
						System.out.println(monGraphe.certificat);
					}
					
					if(commande.startsWith("tc")){
						System.out.println("Entrer votre certificat");
						String certif = stdin.nextLine();
						monGraphe.importeCertificat(certif);
					}
					
					System.out.println(""
							+ "\nch   - Chercher un cycle hamiltonien"
							+ "\nac   - Affiche le cycle en console"
							+ "\ne    - Exporter le graphe dans un fichier type graphviz"
							+ "\nic   - Importer un certificat pour ce graphe"
							+ "\nv    - Lancer le vérificateur de ce certificat"
							+ "\nvt   - Lancer votre propre certificat depuis l'entré clavier"
							+ "\nexit - quitter");
					
					commande = stdin.nextLine();
				}
				commande = " ";
			}else if(commande.startsWith("r")){
				
				System.out.println("Importer expression booleenne : ");
				
				String[] mesFichiers = file.list(new FilenameFilter() {

					@Override
					public boolean accept(File dir, String name) {
						return name.startsWith("instance-3sat");
					}
				});
				for(int i = 0; i<mesFichiers.length ; ++i){
					System.out.println(i+" - "+mesFichiers[i]);
				}

				commande = stdin.nextLine();
				
				monGraphe = GrapheOriente.expressionTroisSATToGraphe(file.getAbsolutePath()+File.separator+mesFichiers[Integer.parseInt(commande)]);
				
				System.out.println(""
						+ "\nch    - Chercher un cycle hamiltonien"
						+ "\nac    - Affiche le cycle en console"
						+ "\ne     - Exporter le graphe dans un fichier type graphviz"
						+ "\nexit  - quitter");
				
				commande = stdin.nextLine();
				
				while(!commande.startsWith("exit")){
					
					if(commande.startsWith("ch")){
						System.out.println("Le graphe possède un cycle hamiltonien : "+monGraphe.solver());
					}
					
					if(commande.startsWith("ac")){
						if(monGraphe.cycle.size()>0){
							monGraphe.solver();
						}
						System.out.println("Cycle : "+monGraphe.cycle);
					}
					
					if(commande.startsWith("e")){
						monGraphe.exportGraphviz();
					}
					
					System.out.println(""
							+ "\nch   - Chercher un cycle hamiltonien"
							+ "\nac   - Affiche le cycle en console"
							+ "\ne    - Exporter le graphe dans un fichier type graphviz"
							+ "\nexit - quitter");
					
					commande = stdin.nextLine();
				}
				commande = " ";

			}else
			{
				System.out.println("Que voulez vous faire ?"
						+ "\ni    - Importer un graphe depuis un fichier (type graphviz)"
						+ "\nr    - Réduire une expression booleene contenue dans un fichier"
						+ "\nexit - quitter");
				
				commande  = stdin.nextLine();
			}
			
		}
		
		stdin.close();
		
	}
}
